/*  Novelties: A visual novel programming language based on JavaFX
    Copyright (C) 2008  Hao Xu

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
 * /
/*
 * ClauseMap.fx
 *
 * Created on Apr 13, 2008, 3:59:44 PM
 */

package avgengine.pred;

import avgengine.script.*;

/**
 * @author ertri
 */



class Assignment {
    attribute
    variable: Variable;
    attribute val: Term;
}

class QueryResult {
    attribute clause: Clause;
    attribute sub: Substitution;
}
class ClauseMap {
    attribute var_base:String;
    attribute var_counter:int;
    attribute clauses:Clause*;
    attribute vnfx:VNFX;
    operation newVar():Variable;
    operation addClause(c:Clause);
    operation getClauses(l:Literal):QueryResult*;
    operation query(c:Literal*):Substitution*;
    operation queryLiteral(l:Literal):Substitution*;
    
}

attribute ClauseMap.var_base="@Var";

operation ClauseMap.newVar() {
    return new Variable{n:"{var_base}{var_counter++}"};
}

operation ClauseMap.queryLiteral(l:Literal):Substitution* {
    var comp = Computible{};
    var ll = comp.computeFoldLiteral(l,vnfx);
    if(ll.p instanceof Bool) {
        if(((Bool)ll.p).bool) {
            return [ Substitution{} ];
        }else {
            return [];
        }
    }
    var res = this.getClauses(ll);
    var subs:Substitution* = [];
    for(i in res) {
        for(r in query(i.clause.tail)) {
            insert i.sub.subSub(r) into subs;
        }
    }
    return subs;
}
operation ClauseMap.addClause(c) {
    insert c into clauses;
}
operation ClauseMap.getClauses(l) {
    var subs:QueryResult* = [];
    var sub;
    for(c in clauses) {
        sub = l.unify(c.head);
//        println("s:{sub},{subs},{l.params[0]},{c.head.params[0]}");
        if(sub == null) {
            continue;
        }
        var fv = c.head.fv(c.tail);
        for(v in fv) {
            
            sub.add(v, newVar());
        }
        insert QueryResult{
            clause:Clause {
                head: sub.subLiteral(c.head)
                tail: sub.subLiterals(c.tail)
            }
            sub: sub
        } into subs;
//        println("e:{sub},{subs}");
    }
    return subs;
}

operation ClauseMap.query(c:Literal*) {
    if(sizeof c == 0) {
        return [Substitution{}];
    }
    var res:Substitution* = [];
    var subs = queryLiteral(c[0]);
    for(sub in subs) {
        var lits = c[n|indexof n > 0];
        lits = sub.subLiterals(lits);
        res = [res,query(lits)];
        
    }
    return res;
}
